a:, n:. |a rem n| < |n| 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), T, P  Q, P & Q, P  Q, P  Q, |i|, True, ff, if b then t else f fi , , tt, False, A, a  b  T , i  j , , , Unit, , A  B, P  Q, Dec(P), , , S  T
Lemmas	nat wf, nat plus wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf, rem bounds 1, absval wf, decidable le, rem sym 1, minus minus cancel, nat plus inc int nzero, absval sym, int nzero wf, rem sym 2